L:Realizer List. (A,BL.A || B)  (AL. R-Feasible(A))  R-Feasible((L)) 

latex

Definitions	x:A. B(x), t  T, P  Q, (x,yL.P(x;y)), xL. P(x), R-Feasible(R), (L), ||as||, True, reduce(f;k;as), Y, Prop, AB, A, False, P & Q, x. t(x), x,y. t(x;y), A || B, if b t else f fi, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), true, {i..j}, i  j < k, P  Q, x(s), x(s1,s2)
Lemmas	es realizer wf, l member wf, R-Feasible wf, int seg wf, R-compat wf, select wf, length wf2, l all cons, pairwise-cons, l all wf, pairwise wf, R-compat-symmetry, Rlist wf, R-compat-none